Commentary by cpressey on Lambda Calculus works
===============================================

<!--
Copyright (c) 2025 Chris Pressey, Cat's Eye Technologies.

SPDX-License-Identifier: CC-BY-ND-4.0
-->

### The Calculi of Lambda-Conversion


### Introduction to Combinators and the Lambda Calculus

Barendregt 1984 should be on this list but isn't.  So, this is.


### A Short Introduction to the Lambda Calculus

A fixed-point combinator can be given (the Y combinator), but
in the simply-typed lambda calculus, it cannot be given a
type.  Thus recursion cannot be done in the STLC and thus the
STLC is not Turing-complete.


### Introduction to Lambda Calculus

This is where I found out about Combinatory Reduction Systems from.


### Chapter 5: The Untyped Lambda Calculus


### Untyped Lambda Calculus


### A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure

So one thing I haven't wrapped my head around here, is that this lambda calculus has
abstractions that take a list of parameters, instead of one abstraction each; which is
a lot more like a conventional programming language (with functions but no currying by
default).  And this is isomorphic to the sequent calculus?  Does this mean anything?


### The Lambda Calculus is Algebraic

"Yes, but what IS an indeterminate?"


### A Lambda Calculus with Naive Substitution

This paper is cited in something else I read -- possibly "Equational Logic as a Programming Language".

I have read this paper, although maybe I missed the point when I did.

Basically, the substitution operator substitutes using a list of positions, rather than a name?
This seems underwhelming.


### A Graph-like Lambda Calculus for which Leftmost-Outermost Reduction is Optimal

I read this, but not entirely comprehendingly -- I could stand to read it again.

This paper is cited in "Equational Logic as a Programming Language".

Staples gives top-level rules for beta-reduction of the lambda calculus (after it has been converted to de Bruijn indexes)
which are essentially algebraic-looking, and which resemble the S, K, I combinators:

    (\x.x G) -> G
    (\x.y G) -> y   (where y =/= x)
    (\x.(E F) G) -> ((\x.E G) (\x.F G))
    (\x.\y.E G) -> (\y.(\x E G))

Which seems to imply that you can derive the S, K, I combinators from analyzing the lambda calculus algebraically.

Which seems weird, because I thought the S, K, I combinators came originally from (Schoenfinkel) taking
that basic axiom system of Hilbert's and making them "point-free".

But weirder things have happened.  So, OK.


### On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control

For a long time it has been widely thought that a classical proof, as opposed to an intuitionistic one,
did not carry any computational content... but!  Types-as-propositions.

I guess by "Syntactic Theory of Sequential Control" they refer to continuations.


### functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange


### What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange


### lo.logic - What\'s the point of \$\\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange


### lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange


### lo.logic - Scott on the consistency of the lambda calculus - MathOverflow


### Lambda Terms


### The largest number representable in 64 bits


### lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow


### maciej-bendkowski/lambda-sampler: Boltzmann sampler utilities for lambda calculus